(set-logic BV)
(synth-fun f ( (x (BitVec 64)) ) (BitVec 64)
((Start (BitVec 64)
((bvnot Start)
(bvxor Start Start)
(bvand Start Start)
(bvor Start Start)
(bvneg Start)
(bvadd Start Start)
(bvmul Start Start)
(bvudiv Start Start)
(bvurem Start Start)
(bvlshr Start Start)
(bvashr Start Start)
(bvshl Start Start)
(bvsdiv Start Start)
(bvsrem Start Start)
(bvsub Start Start)
x
#x0000000000000000
#x0000000000000001
#x0000000000000002
#x0000000000000003
#x0000000000000004
#x0000000000000005
#x0000000000000006
#x0000000000000007
#x0000000000000008
#x0000000000000009
#x0000000000000009
#x0000000000000009
#x000000000000000A
#x000000000000000B
#x000000000000000C
#x000000000000000D
#x000000000000000E
#x000000000000000F
#x0000000000000010
(ite StartBool Start Start)
))
(StartBool Bool
((= Start Start)
(not StartBool)
(and StartBool StartBool)
(or StartBool StartBool)
))))
(constraint (= (f #xe14ab19838e9b83a) #x0000000000000000))
(constraint (= (f #xcae70634b74a5e76) #x00000cae70634b74))
(constraint (= (f #x8031dcd5427bc991) #x0000319880427901))
(constraint (= (f #x05ec2ed9108b7d38) #x0000000000000000))
(constraint (= (f #xd420e09393e3eab5) #x0084000012106143))
(constraint (= (f #x6be7483352c0b05a) #x000006be7483352c))
(constraint (= (f #x8702097e903e2c41) #x0080000952000409))
(constraint (= (f #x12d9d631bd952865) #x001218c631b08509))
(constraint (= (f #xea825035878d0126) #x0000000000000000))
(constraint (= (f #xceb2173be53057e5) #x00c6020738a40055))
(constraint (= (f #x3a37922d6eb5e13c) #x0000000000000000))
(constraint (= (f #x820e342a0a1357ce) #x0000000000000000))
(constraint (= (f #x9ccce2c90963c5e4) #x0000000000000000))
(constraint (= (f #x1e378a1e8e8080c1) #x0006310210800001))
(constraint (= (f #x71e0d794ce312e6d) #x003000d290c6210d))
(constraint (= (f #x712a75d603524429) #x00210a30c0024005))
(constraint (= (f #x1673dc95d4cd28c5) #x0006739090908509))
(constraint (= (f #x0744be1e43e390aa) #x0000000000000000))
(constraint (= (f #x500452b98d1a018c) #x00000500452b98d1))
(constraint (= (f #x45a69b870a11edd4) #x0000000000000000))
(constraint (= (f #x44c7c301eac02076) #x0000044c7c301eac))
(constraint (= (f #xb3d34d5c4a8b2a0e) #x0000000000000000))
(constraint (= (f #x273b837a118ada05) #x0027300342110a41))
(constraint (= (f #x01bb87ad6984c76d) #x00013085ad2080c6))
(constraint (= (f #x015427b6572a9e0e) #x00000015427b6572))
(constraint (= (f #x624bb06ea308606e) #x00000624bb06ea30))
(constraint (= (f #x4d49d81cca7c90c3) #x00090900184a1011))
(constraint (= (f #x05944cbb2cb1cae7) #x0000800421043149))
(constraint (= (f #x19d12e151ae826bc) #x0000019d12e151ae))
(constraint (= (f #x679e5b352db7661a) #x0000000000000000))
(constraint (= (f #xe9ddabeca523b61b) #x0029952984a42283))
(constraint (= (f #xcda130921c9e392a) #x00000cda130921c9))
(constraint (= (f #xa4241e7ccce027cb) #x0084000e188c0022))
(constraint (= (f #x41eeea5728551d90) #x0000000000000000))
(constraint (= (f #xe348001a7a76da90) #x00000e348001a7a7))
(constraint (= (f #xc4938c2003eca126) #x00000c4938c2003e))
(constraint (= (f #xb7e316e607e5b8ee) #x0000000000000000))
(constraint (= (f #xd4623c90689473e4) #x00000d4623c90689))
(constraint (= (f #x4a212dab6d3c953e) #x000004a212dab6d3))
(constraint (= (f #xb697948e03588bad) #x0092929080031002))
(constraint (= (f #xb50bda0602dee3d4) #x00000b50bda0602d))
(constraint (= (f #xd67157de70e4023b) #x00c62053ce108003))
(constraint (= (f #xe3c90e951e2b4c43) #x0061010281042909))
(constraint (= (f #x13ee3d0ab42ce50c) #x0000013ee3d0ab42))
(constraint (= (f #xb96d46d965c4d011) #x0029284208208001))
(constraint (= (f #xc83010ab39b5b4cb) #x000000102330b491))
(constraint (= (f #x273895a4c20c9e0b) #x0027109480400081))
(constraint (= (f #xe1ae99376e4a1ae9) #x0021820025484219))
(constraint (= (f #x07ba4043e974337e) #x0000007ba4043e97))
(constraint (= (f #x2799cc4ea0d6526e) #x000002799cc4ea0d))
(constraint (= (f #xbe71e34e51d95d4e) #x0000000000000000))
(constraint (= (f #x5681177e59098c2a) #x0000000000000000))
(constraint (= (f #xdabdc2ded8731c77) #x0052b842da08630d))
(constraint (= (f #x6dcde19e50005471) #x00298c218a000005))
(constraint (= (f #x64225106e4ed4cae) #x0000000000000000))
(constraint (= (f #x822a9c3e5116c713) #x000002840a0010c3))
(constraint (= (f #xe5ee3b8737a67944) #x00000e5ee3b8737a))
(constraint (= (f #x9d79830175b639b8) #x000009d79830175b))
(constraint (= (f #x7ede5445b5365e35) #x005aca0004a40247))
(constraint (= (f #xbba859bd35a4bdce) #x00000bba859bd35a))
(constraint (= (f #xe5beb88524e7ead1) #x00a596108404e54b))
(constraint (= (f #xe946d98de2aae361) #x002842118c400861))
(constraint (= (f #x39a5914bee679ee1) #x0030a00149cc639d))
(constraint (= (f #xa7ea45b3c9e17c61) #x00a548043108210d))
(constraint (= (f #x68a02b230869b8aa) #x0000000000000000))
(constraint (= (f #x08e224554890b197) #x0008400001001031))
(constraint (= (f #x4325e096eb4099e9) #x004024009468001a))
(constraint (= (f #x63055e4da749ad63) #x0060014804a101ad))
(constraint (= (f #xed6dc4ee8e73bdc2) #x0000000000000000))
(constraint (= (f #xaaecc8b9c1d50eac) #x0000000000000000))
(constraint (= (f #xe2340b55b76c2689) #x0042000a14a50401))
(constraint (= (f #x560500b376b2a6a4) #x00000560500b376b))
(constraint (= (f #x4b5ed4d63eae7c7e) #x000004b5ed4d63ea))
(constraint (= (f #xc9376bc5495016c5) #x0000256881080011))
(constraint (= (f #xe6a7126a9079d500) #x0000000000000000))
(constraint (= (f #x1398c36e29b9ca06) #x0000000000000000))
(constraint (= (f #x2ae683c6ee56be8e) #x000002ae683c6ee5))
(constraint (= (f #xe54e2dadeae7eb14) #x0000000000000000))
(constraint (= (f #x5d559e5ebc7861c3) #x0008118a568c0821))
(constraint (= (f #xd3117328988b18e1) #x0042006100100319))
(constraint (= (f #x96647dda1eb8e168) #x0000096647dda1eb))
(constraint (= (f #x82d48186892e82d4) #x0000082d48186892))
(constraint (= (f #xd4c6b5dc53180c3e) #x00000d4c6b5dc531))
(constraint (= (f #x6beb6e8eb34d387c) #x0000000000000000))
(constraint (= (f #x76c985dee5983de2) #x0000076c985dee59))
(constraint (= (f #x962ce6cc75db19ba) #x0000000000000000))
(constraint (= (f #xe3ee950b464cc9c7) #x0061c28108400809))
(constraint (= (f #x114534ac0195708d) #x0000041480008411))
(constraint (= (f #x0043b1a90ae93372) #x0000000000000000))
(constraint (= (f #x9e577c27eae5e935) #x008a47042548a521))
(constraint (= (f #xebcaaa8b316d073e) #x0000000000000000))
(constraint (= (f #xe8d1e135e9eee055) #x000810203529cc01))
(constraint (= (f #xc733b4e58186cc7b) #x00c63294a000808d))
(constraint (= (f #x36d828a253cb3695) #x0012000002514213))
(constraint (= (f #x4aeee4292024e928) #x000004aeee429202))
(constraint (= (f #xb713bbbe95aea34c) #x00000b713bbbe95a))
(constraint (= (f #x9b6ebe22e8b17e05) #x0009468400002141))
(constraint (= (f #x61ee87bb3be51c7d) #x0021c0872338a10d))
(constraint (= (f #x2a55ee14a640b58d) #x000a15c2148000b2))
(constraint (= (f #x9c7994ed60c15367) #x008c3094ac000041))
(check-synth)
